\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$).
\-\\[0ex]update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ msg{-}spec{-}loc{-}decl(${\it snd}$; $i$; ${\it da}$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ R{-}Feasible\=\{i:l\}\+
\\[0ex](ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$))
\-\\[0ex]$\Rightarrow$ \=(\=$\forall$$k$:Knd, ${\it ds}_{2}$:fpf(Id; $x$.Type), $T$:Type, $x$:Id,\+\+
\\[0ex]$f$:(\=(decl{-}state(${\it ds}_{2}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+\+
\\[0ex](${\it ds}_{2}$; $x$)) + (decl{-}state(${\it ds}_{2}$)$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$
\-\\[0ex]decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}_{2}$; $x$))).
\-\-\-\\[0ex]($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}_{2}$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$eq\_id(mkid\{ecl:ut2\}; $x$)))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; ${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ fpf{-}compatible(Knd; $k$.Type; Kind{-}deq; ${\it da}$; fpf{-}single($k$; $T$))
\\[0ex]$\Rightarrow$ (($k$ $\in$ ecl{-}kinds($A$)) $\Rightarrow$ ((ma{-}valtype(${\it da}$; $k$) = $T$) $\wedge$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$))))
\\[0ex]$\Rightarrow$ ($\neg$($x$ $\in$ update{-}spec{-}vars(${\it upd}$)))
\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$); Reffect($i$; ${\it ds}_{2}$; $k$; $T$; $x$; $f$)))
\-\-
\end{tabbing}